MAYBE 20.903
H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could not be shown:
↳ HASKELL
↳ BR
mainModule Main
| ((enumFromThenTo :: Int -> Int -> Int -> [Int]) :: Int -> Int -> Int -> [Int]) |
module Main where
Replaced joker patterns by fresh variables and removed binding patterns.
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
mainModule Main
| ((enumFromThenTo :: Int -> Int -> Int -> [Int]) :: Int -> Int -> Int -> [Int]) |
module Main where
Cond Reductions:
The following Function with conditions
is transformed to
undefined0 | True | = undefined |
undefined1 | | = undefined0 False |
The following Function with conditions
is transformed to
p1 | True | = flip (<=) m |
p1 | False | = p0 otherwise |
The following Function with conditions
takeWhile | p [] | = [] |
takeWhile | p (x : xs) | |
is transformed to
takeWhile | p [] | = takeWhile3 p [] |
takeWhile | p (x : xs) | = takeWhile2 p (x : xs) |
takeWhile0 | p x xs True | = [] |
takeWhile1 | p x xs True | = x : takeWhile p xs |
takeWhile1 | p x xs False | = takeWhile0 p x xs otherwise |
takeWhile2 | p (x : xs) | = takeWhile1 p x xs (p x) |
takeWhile3 | p [] | = [] |
takeWhile3 | vz wu | = takeWhile2 vz wu |
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
mainModule Main
| ((enumFromThenTo :: Int -> Int -> Int -> [Int]) :: Int -> Int -> Int -> [Int]) |
module Main where
Let/Where Reductions:
The bindings of the following Let/Where expression
takeWhile p (numericEnumFromThen n n') |
where | |
| |
|
p1 | True | = flip (<=) m |
p1 | False | = p0 otherwise |
|
| |
are unpacked to the following functions on top level
numericEnumFromThenToP0 | wv ww wx True | = flip (>=) wv |
numericEnumFromThenToP1 | wv ww wx True | = flip (<=) wv |
numericEnumFromThenToP1 | wv ww wx False | = numericEnumFromThenToP0 wv ww wx otherwise |
numericEnumFromThenToP | wv ww wx | = numericEnumFromThenToP2 wv ww wx |
numericEnumFromThenToP2 | wv ww wx | = numericEnumFromThenToP1 wv ww wx (ww >= wx) |
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ Narrow
mainModule Main
| (enumFromThenTo :: Int -> Int -> Int -> [Int]) |
module Main where
Haskell To QDPs
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ Narrow
Q DP problem:
The TRS P consists of the following rules:
new_primMinusNat(Succ(wy9200), Succ(wy3900)) → new_primMinusNat(wy9200, wy3900)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primMinusNat(Succ(wy9200), Succ(wy3900)) → new_primMinusNat(wy9200, wy3900)
The graph contains the following edges 1 > 1, 2 > 2
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ Narrow
Q DP problem:
The TRS P consists of the following rules:
new_primPlusNat(Succ(wy9200), Succ(wy3900)) → new_primPlusNat(wy9200, wy3900)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primPlusNat(Succ(wy9200), Succ(wy3900)) → new_primPlusNat(wy9200, wy3900)
The graph contains the following edges 1 > 1, 2 > 2
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ Rewriting
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ Narrow
Q DP problem:
The TRS P consists of the following rules:
new_iterate(wy165, wy164, wy163) → new_iterate(wy165, wy165, new_ps(wy164, wy163))
The TRS R consists of the following rules:
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusInt(Pos(wy920), Pos(wy390)) → Pos(new_primPlusNat0(wy920, wy390))
new_primMinusNat0(Zero, Zero) → Pos(Zero)
new_primPlusInt(Neg(wy920), Neg(wy390)) → Neg(new_primPlusNat0(wy920, wy390))
new_primMinusNat0(Succ(wy9200), Zero) → Pos(Succ(wy9200))
new_primMinusNat0(Zero, Succ(wy3900)) → Neg(Succ(wy3900))
new_primPlusNat0(Zero, Succ(wy3900)) → Succ(wy3900)
new_primPlusNat0(Succ(wy9200), Zero) → Succ(wy9200)
new_primPlusNat0(Succ(wy9200), Succ(wy3900)) → Succ(Succ(new_primPlusNat0(wy9200, wy3900)))
new_ps(wy164, wy163) → new_primPlusInt(wy164, wy163)
new_primPlusInt(Neg(wy920), Pos(wy390)) → new_primMinusNat0(wy390, wy920)
new_primPlusInt(Pos(wy920), Neg(wy390)) → new_primMinusNat0(wy920, wy390)
new_primMinusNat0(Succ(wy9200), Succ(wy3900)) → new_primMinusNat0(wy9200, wy3900)
The set Q consists of the following terms:
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Zero)
new_ps(x0, x1)
new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusInt(Pos(x0), Neg(x1))
new_primPlusInt(Neg(x0), Pos(x1))
new_primPlusNat0(Zero, Zero)
new_primMinusNat0(Zero, Zero)
new_primMinusNat0(Zero, Succ(x0))
new_primPlusInt(Neg(x0), Neg(x1))
new_primMinusNat0(Succ(x0), Zero)
new_primPlusInt(Pos(x0), Pos(x1))
new_primMinusNat0(Succ(x0), Succ(x1))
We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule new_iterate(wy165, wy164, wy163) → new_iterate(wy165, wy165, new_ps(wy164, wy163)) at position [2] we obtained the following new rules:
new_iterate(wy165, wy164, wy163) → new_iterate(wy165, wy165, new_primPlusInt(wy164, wy163))
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ Narrow
Q DP problem:
The TRS P consists of the following rules:
new_iterate(wy165, wy164, wy163) → new_iterate(wy165, wy165, new_primPlusInt(wy164, wy163))
The TRS R consists of the following rules:
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusInt(Pos(wy920), Pos(wy390)) → Pos(new_primPlusNat0(wy920, wy390))
new_primMinusNat0(Zero, Zero) → Pos(Zero)
new_primPlusInt(Neg(wy920), Neg(wy390)) → Neg(new_primPlusNat0(wy920, wy390))
new_primMinusNat0(Succ(wy9200), Zero) → Pos(Succ(wy9200))
new_primMinusNat0(Zero, Succ(wy3900)) → Neg(Succ(wy3900))
new_primPlusNat0(Zero, Succ(wy3900)) → Succ(wy3900)
new_primPlusNat0(Succ(wy9200), Zero) → Succ(wy9200)
new_primPlusNat0(Succ(wy9200), Succ(wy3900)) → Succ(Succ(new_primPlusNat0(wy9200, wy3900)))
new_ps(wy164, wy163) → new_primPlusInt(wy164, wy163)
new_primPlusInt(Neg(wy920), Pos(wy390)) → new_primMinusNat0(wy390, wy920)
new_primPlusInt(Pos(wy920), Neg(wy390)) → new_primMinusNat0(wy920, wy390)
new_primMinusNat0(Succ(wy9200), Succ(wy3900)) → new_primMinusNat0(wy9200, wy3900)
The set Q consists of the following terms:
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Zero)
new_ps(x0, x1)
new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusInt(Pos(x0), Neg(x1))
new_primPlusInt(Neg(x0), Pos(x1))
new_primPlusNat0(Zero, Zero)
new_primMinusNat0(Zero, Zero)
new_primMinusNat0(Zero, Succ(x0))
new_primPlusInt(Neg(x0), Neg(x1))
new_primMinusNat0(Succ(x0), Zero)
new_primPlusInt(Pos(x0), Pos(x1))
new_primMinusNat0(Succ(x0), Succ(x1))
We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ Narrow
Q DP problem:
The TRS P consists of the following rules:
new_iterate(wy165, wy164, wy163) → new_iterate(wy165, wy165, new_primPlusInt(wy164, wy163))
The TRS R consists of the following rules:
new_primPlusInt(Pos(wy920), Pos(wy390)) → Pos(new_primPlusNat0(wy920, wy390))
new_primPlusInt(Neg(wy920), Neg(wy390)) → Neg(new_primPlusNat0(wy920, wy390))
new_primPlusInt(Neg(wy920), Pos(wy390)) → new_primMinusNat0(wy390, wy920)
new_primPlusInt(Pos(wy920), Neg(wy390)) → new_primMinusNat0(wy920, wy390)
new_primMinusNat0(Zero, Zero) → Pos(Zero)
new_primMinusNat0(Succ(wy9200), Zero) → Pos(Succ(wy9200))
new_primMinusNat0(Zero, Succ(wy3900)) → Neg(Succ(wy3900))
new_primMinusNat0(Succ(wy9200), Succ(wy3900)) → new_primMinusNat0(wy9200, wy3900)
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat0(Zero, Succ(wy3900)) → Succ(wy3900)
new_primPlusNat0(Succ(wy9200), Zero) → Succ(wy9200)
new_primPlusNat0(Succ(wy9200), Succ(wy3900)) → Succ(Succ(new_primPlusNat0(wy9200, wy3900)))
The set Q consists of the following terms:
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Zero)
new_ps(x0, x1)
new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusInt(Pos(x0), Neg(x1))
new_primPlusInt(Neg(x0), Pos(x1))
new_primPlusNat0(Zero, Zero)
new_primMinusNat0(Zero, Zero)
new_primMinusNat0(Zero, Succ(x0))
new_primPlusInt(Neg(x0), Neg(x1))
new_primMinusNat0(Succ(x0), Zero)
new_primPlusInt(Pos(x0), Pos(x1))
new_primMinusNat0(Succ(x0), Succ(x1))
We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.
new_ps(x0, x1)
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Instantiation
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ Narrow
Q DP problem:
The TRS P consists of the following rules:
new_iterate(wy165, wy164, wy163) → new_iterate(wy165, wy165, new_primPlusInt(wy164, wy163))
The TRS R consists of the following rules:
new_primPlusInt(Pos(wy920), Pos(wy390)) → Pos(new_primPlusNat0(wy920, wy390))
new_primPlusInt(Neg(wy920), Neg(wy390)) → Neg(new_primPlusNat0(wy920, wy390))
new_primPlusInt(Neg(wy920), Pos(wy390)) → new_primMinusNat0(wy390, wy920)
new_primPlusInt(Pos(wy920), Neg(wy390)) → new_primMinusNat0(wy920, wy390)
new_primMinusNat0(Zero, Zero) → Pos(Zero)
new_primMinusNat0(Succ(wy9200), Zero) → Pos(Succ(wy9200))
new_primMinusNat0(Zero, Succ(wy3900)) → Neg(Succ(wy3900))
new_primMinusNat0(Succ(wy9200), Succ(wy3900)) → new_primMinusNat0(wy9200, wy3900)
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat0(Zero, Succ(wy3900)) → Succ(wy3900)
new_primPlusNat0(Succ(wy9200), Zero) → Succ(wy9200)
new_primPlusNat0(Succ(wy9200), Succ(wy3900)) → Succ(Succ(new_primPlusNat0(wy9200, wy3900)))
The set Q consists of the following terms:
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusInt(Pos(x0), Neg(x1))
new_primPlusInt(Neg(x0), Pos(x1))
new_primPlusNat0(Zero, Zero)
new_primMinusNat0(Zero, Zero)
new_primMinusNat0(Zero, Succ(x0))
new_primPlusInt(Neg(x0), Neg(x1))
new_primMinusNat0(Succ(x0), Zero)
new_primPlusInt(Pos(x0), Pos(x1))
new_primMinusNat0(Succ(x0), Succ(x1))
We have to consider all minimal (P,Q,R)-chains.
By instantiating [15] the rule new_iterate(wy165, wy164, wy163) → new_iterate(wy165, wy165, new_primPlusInt(wy164, wy163)) we obtained the following new rules:
new_iterate(z0, z0, y_0) → new_iterate(z0, z0, new_primPlusInt(z0, y_0))
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Instantiation
↳ QDP
↳ MNOCProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ Narrow
Q DP problem:
The TRS P consists of the following rules:
new_iterate(z0, z0, y_0) → new_iterate(z0, z0, new_primPlusInt(z0, y_0))
The TRS R consists of the following rules:
new_primPlusInt(Pos(wy920), Pos(wy390)) → Pos(new_primPlusNat0(wy920, wy390))
new_primPlusInt(Neg(wy920), Neg(wy390)) → Neg(new_primPlusNat0(wy920, wy390))
new_primPlusInt(Neg(wy920), Pos(wy390)) → new_primMinusNat0(wy390, wy920)
new_primPlusInt(Pos(wy920), Neg(wy390)) → new_primMinusNat0(wy920, wy390)
new_primMinusNat0(Zero, Zero) → Pos(Zero)
new_primMinusNat0(Succ(wy9200), Zero) → Pos(Succ(wy9200))
new_primMinusNat0(Zero, Succ(wy3900)) → Neg(Succ(wy3900))
new_primMinusNat0(Succ(wy9200), Succ(wy3900)) → new_primMinusNat0(wy9200, wy3900)
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat0(Zero, Succ(wy3900)) → Succ(wy3900)
new_primPlusNat0(Succ(wy9200), Zero) → Succ(wy9200)
new_primPlusNat0(Succ(wy9200), Succ(wy3900)) → Succ(Succ(new_primPlusNat0(wy9200, wy3900)))
The set Q consists of the following terms:
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusInt(Pos(x0), Neg(x1))
new_primPlusInt(Neg(x0), Pos(x1))
new_primPlusNat0(Zero, Zero)
new_primMinusNat0(Zero, Zero)
new_primMinusNat0(Zero, Succ(x0))
new_primPlusInt(Neg(x0), Neg(x1))
new_primMinusNat0(Succ(x0), Zero)
new_primPlusInt(Pos(x0), Pos(x1))
new_primMinusNat0(Succ(x0), Succ(x1))
We have to consider all minimal (P,Q,R)-chains.
We use the modular non-overlap check [17] to decrease Q to the empty set.
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Instantiation
↳ QDP
↳ MNOCProof
↳ QDP
↳ NonTerminationProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ Narrow
Q DP problem:
The TRS P consists of the following rules:
new_iterate(z0, z0, y_0) → new_iterate(z0, z0, new_primPlusInt(z0, y_0))
The TRS R consists of the following rules:
new_primPlusInt(Pos(wy920), Pos(wy390)) → Pos(new_primPlusNat0(wy920, wy390))
new_primPlusInt(Neg(wy920), Neg(wy390)) → Neg(new_primPlusNat0(wy920, wy390))
new_primPlusInt(Neg(wy920), Pos(wy390)) → new_primMinusNat0(wy390, wy920)
new_primPlusInt(Pos(wy920), Neg(wy390)) → new_primMinusNat0(wy920, wy390)
new_primMinusNat0(Zero, Zero) → Pos(Zero)
new_primMinusNat0(Succ(wy9200), Zero) → Pos(Succ(wy9200))
new_primMinusNat0(Zero, Succ(wy3900)) → Neg(Succ(wy3900))
new_primMinusNat0(Succ(wy9200), Succ(wy3900)) → new_primMinusNat0(wy9200, wy3900)
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat0(Zero, Succ(wy3900)) → Succ(wy3900)
new_primPlusNat0(Succ(wy9200), Zero) → Succ(wy9200)
new_primPlusNat0(Succ(wy9200), Succ(wy3900)) → Succ(Succ(new_primPlusNat0(wy9200, wy3900)))
Q is empty.
We have to consider all (P,Q,R)-chains.
We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.
The TRS P consists of the following rules:
new_iterate(z0, z0, y_0) → new_iterate(z0, z0, new_primPlusInt(z0, y_0))
The TRS R consists of the following rules:
new_primPlusInt(Pos(wy920), Pos(wy390)) → Pos(new_primPlusNat0(wy920, wy390))
new_primPlusInt(Neg(wy920), Neg(wy390)) → Neg(new_primPlusNat0(wy920, wy390))
new_primPlusInt(Neg(wy920), Pos(wy390)) → new_primMinusNat0(wy390, wy920)
new_primPlusInt(Pos(wy920), Neg(wy390)) → new_primMinusNat0(wy920, wy390)
new_primMinusNat0(Zero, Zero) → Pos(Zero)
new_primMinusNat0(Succ(wy9200), Zero) → Pos(Succ(wy9200))
new_primMinusNat0(Zero, Succ(wy3900)) → Neg(Succ(wy3900))
new_primMinusNat0(Succ(wy9200), Succ(wy3900)) → new_primMinusNat0(wy9200, wy3900)
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat0(Zero, Succ(wy3900)) → Succ(wy3900)
new_primPlusNat0(Succ(wy9200), Zero) → Succ(wy9200)
new_primPlusNat0(Succ(wy9200), Succ(wy3900)) → Succ(Succ(new_primPlusNat0(wy9200, wy3900)))
s = new_iterate(z0, z0, y_0) evaluates to t =new_iterate(z0, z0, new_primPlusInt(z0, y_0))
Thus s starts an infinite chain as s semiunifies with t with the following substitutions:
- Semiunifier: [ ]
- Matcher: [y_0 / new_primPlusInt(z0, y_0)]
Rewriting sequence
The DP semiunifies directly so there is only one rewrite step from new_iterate(z0, z0, y_0) to new_iterate(z0, z0, new_primPlusInt(z0, y_0)).
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ Narrow
Q DP problem:
The TRS P consists of the following rules:
new_takeWhile10(wy2180, wy220, wy223) → new_takeWhile1(wy2180, Pos(Succ(wy220)), wy223)
new_takeWhile13(wy361, wy362, wy363, Zero, Zero) → new_takeWhile14(wy361, wy362, wy363)
new_takeWhile1(Zero, wy105, :(Pos(Zero), wy2871)) → new_takeWhile1(Zero, Pos(Zero), wy2871)
new_takeWhile13(wy361, wy362, wy363, Succ(wy3640), Succ(wy3650)) → new_takeWhile13(wy361, wy362, wy363, wy3640, wy3650)
new_takeWhile12(Succ(wy23500), wy237, wy240) → new_takeWhile13(wy23500, Neg(Succ(wy237)), wy240, wy23500, wy237)
new_takeWhile1(Succ(wy500), wy105, :(Pos(Zero), wy2871)) → new_takeWhile11(wy500, Pos(Zero), wy2871)
new_takeWhile1(Zero, wy105, :(Neg(Zero), wy2871)) → new_takeWhile1(Zero, Neg(Zero), wy2871)
new_takeWhile1(Succ(wy500), wy105, :(Neg(Zero), wy2871)) → new_takeWhile13(wy500, Neg(Zero), wy2871, Succ(wy500), Zero)
new_takeWhile13(wy361, wy362, wy363, Succ(wy3640), Zero) → new_takeWhile11(wy361, wy362, wy363)
new_takeWhile11(wy500, wy186, wy185) → new_takeWhile1(Succ(wy500), wy186, wy185)
new_takeWhile14(wy500, wy186, wy185) → new_takeWhile1(Succ(wy500), wy186, wy185)
new_takeWhile1(wy50, wy105, :(Neg(Succ(wy287000)), wy2871)) → new_takeWhile12(wy50, wy287000, wy2871)
new_takeWhile1(wy50, wy105, :(Pos(Succ(wy287000)), wy2871)) → new_takeWhile10(wy50, wy287000, wy2871)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_takeWhile1(wy50, wy105, :(Pos(Succ(wy287000)), wy2871)) → new_takeWhile10(wy50, wy287000, wy2871)
The graph contains the following edges 1 >= 1, 3 > 2, 3 > 3
- new_takeWhile14(wy500, wy186, wy185) → new_takeWhile1(Succ(wy500), wy186, wy185)
The graph contains the following edges 2 >= 2, 3 >= 3
- new_takeWhile1(wy50, wy105, :(Neg(Succ(wy287000)), wy2871)) → new_takeWhile12(wy50, wy287000, wy2871)
The graph contains the following edges 1 >= 1, 3 > 2, 3 > 3
- new_takeWhile10(wy2180, wy220, wy223) → new_takeWhile1(wy2180, Pos(Succ(wy220)), wy223)
The graph contains the following edges 1 >= 1, 3 >= 3
- new_takeWhile13(wy361, wy362, wy363, Succ(wy3640), Succ(wy3650)) → new_takeWhile13(wy361, wy362, wy363, wy3640, wy3650)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 > 4, 5 > 5
- new_takeWhile12(Succ(wy23500), wy237, wy240) → new_takeWhile13(wy23500, Neg(Succ(wy237)), wy240, wy23500, wy237)
The graph contains the following edges 1 > 1, 3 >= 3, 1 > 4, 2 >= 5
- new_takeWhile11(wy500, wy186, wy185) → new_takeWhile1(Succ(wy500), wy186, wy185)
The graph contains the following edges 2 >= 2, 3 >= 3
- new_takeWhile13(wy361, wy362, wy363, Succ(wy3640), Zero) → new_takeWhile11(wy361, wy362, wy363)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3
- new_takeWhile13(wy361, wy362, wy363, Zero, Zero) → new_takeWhile14(wy361, wy362, wy363)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3
- new_takeWhile1(Succ(wy500), wy105, :(Neg(Zero), wy2871)) → new_takeWhile13(wy500, Neg(Zero), wy2871, Succ(wy500), Zero)
The graph contains the following edges 1 > 1, 3 > 2, 3 > 3, 1 >= 4, 3 > 5
- new_takeWhile1(Succ(wy500), wy105, :(Pos(Zero), wy2871)) → new_takeWhile11(wy500, Pos(Zero), wy2871)
The graph contains the following edges 1 > 1, 3 > 2, 3 > 3
- new_takeWhile1(Zero, wy105, :(Pos(Zero), wy2871)) → new_takeWhile1(Zero, Pos(Zero), wy2871)
The graph contains the following edges 1 >= 1, 3 > 1, 3 > 2, 3 > 3
- new_takeWhile1(Zero, wy105, :(Neg(Zero), wy2871)) → new_takeWhile1(Zero, Neg(Zero), wy2871)
The graph contains the following edges 1 >= 1, 3 > 1, 3 > 2, 3 > 3
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ Narrow
Q DP problem:
The TRS P consists of the following rules:
new_takeWhile19(wy155, :(Pos(Succ(wy265000)), wy2651)) → new_takeWhile16(Zero, wy265000, wy2651)
new_takeWhile19(wy155, :(Pos(Zero), wy2651)) → new_takeWhile19(Pos(Zero), wy2651)
new_takeWhile16(Succ(wy21800), wy220, wy223) → new_takeWhile15(wy21800, wy220, wy223, wy220, wy21800)
new_takeWhile18(wy155, wy264) → new_takeWhile19(wy155, wy264)
new_takeWhile15(wy349, wy350, :(Pos(Succ(wy351000)), wy3511), Succ(wy3520), Zero) → new_takeWhile16(Succ(wy349), wy351000, wy3511)
new_takeWhile15(wy349, wy350, wy351, Zero, Zero) → new_takeWhile17(wy349, wy350, wy351)
new_takeWhile16(Zero, wy220, wy223) → new_takeWhile18(Pos(Succ(wy220)), wy223)
new_takeWhile17(wy349, wy350, :(Pos(Succ(wy351000)), wy3511)) → new_takeWhile16(Succ(wy349), wy351000, wy3511)
new_takeWhile19(wy155, :(Neg(Zero), wy2651)) → new_takeWhile19(Neg(Zero), wy2651)
new_takeWhile15(wy349, wy350, wy351, Succ(wy3520), Succ(wy3530)) → new_takeWhile15(wy349, wy350, wy351, wy3520, wy3530)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 2 SCCs.
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ Narrow
Q DP problem:
The TRS P consists of the following rules:
new_takeWhile16(Succ(wy21800), wy220, wy223) → new_takeWhile15(wy21800, wy220, wy223, wy220, wy21800)
new_takeWhile15(wy349, wy350, :(Pos(Succ(wy351000)), wy3511), Succ(wy3520), Zero) → new_takeWhile16(Succ(wy349), wy351000, wy3511)
new_takeWhile15(wy349, wy350, wy351, Zero, Zero) → new_takeWhile17(wy349, wy350, wy351)
new_takeWhile17(wy349, wy350, :(Pos(Succ(wy351000)), wy3511)) → new_takeWhile16(Succ(wy349), wy351000, wy3511)
new_takeWhile15(wy349, wy350, wy351, Succ(wy3520), Succ(wy3530)) → new_takeWhile15(wy349, wy350, wy351, wy3520, wy3530)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_takeWhile16(Succ(wy21800), wy220, wy223) → new_takeWhile15(wy21800, wy220, wy223, wy220, wy21800)
The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 3, 2 >= 4, 1 > 5
- new_takeWhile15(wy349, wy350, wy351, Succ(wy3520), Succ(wy3530)) → new_takeWhile15(wy349, wy350, wy351, wy3520, wy3530)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 > 4, 5 > 5
- new_takeWhile15(wy349, wy350, :(Pos(Succ(wy351000)), wy3511), Succ(wy3520), Zero) → new_takeWhile16(Succ(wy349), wy351000, wy3511)
The graph contains the following edges 3 > 2, 3 > 3
- new_takeWhile15(wy349, wy350, wy351, Zero, Zero) → new_takeWhile17(wy349, wy350, wy351)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3
- new_takeWhile17(wy349, wy350, :(Pos(Succ(wy351000)), wy3511)) → new_takeWhile16(Succ(wy349), wy351000, wy3511)
The graph contains the following edges 3 > 2, 3 > 3
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ Narrow
Q DP problem:
The TRS P consists of the following rules:
new_takeWhile19(wy155, :(Pos(Zero), wy2651)) → new_takeWhile19(Pos(Zero), wy2651)
new_takeWhile19(wy155, :(Pos(Succ(wy265000)), wy2651)) → new_takeWhile16(Zero, wy265000, wy2651)
new_takeWhile18(wy155, wy264) → new_takeWhile19(wy155, wy264)
new_takeWhile16(Zero, wy220, wy223) → new_takeWhile18(Pos(Succ(wy220)), wy223)
new_takeWhile19(wy155, :(Neg(Zero), wy2651)) → new_takeWhile19(Neg(Zero), wy2651)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_takeWhile16(Zero, wy220, wy223) → new_takeWhile18(Pos(Succ(wy220)), wy223)
The graph contains the following edges 3 >= 2
- new_takeWhile19(wy155, :(Pos(Succ(wy265000)), wy2651)) → new_takeWhile16(Zero, wy265000, wy2651)
The graph contains the following edges 2 > 2, 2 > 3
- new_takeWhile18(wy155, wy264) → new_takeWhile19(wy155, wy264)
The graph contains the following edges 1 >= 1, 2 >= 2
- new_takeWhile19(wy155, :(Pos(Zero), wy2651)) → new_takeWhile19(Pos(Zero), wy2651)
The graph contains the following edges 2 > 1, 2 > 2
- new_takeWhile19(wy155, :(Neg(Zero), wy2651)) → new_takeWhile19(Neg(Zero), wy2651)
The graph contains the following edges 2 > 1, 2 > 2
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDP
↳ QDP
↳ Narrow
Q DP problem:
The TRS P consists of the following rules:
new_takeWhile110(Zero, wy21, wy138) → new_takeWhile(wy138)
new_takeWhile112(wy339, wy340, :(Neg(Succ(wy341000)), wy3411)) → new_takeWhile110(Succ(wy339), wy341000, wy3411)
new_takeWhile113(:(Neg(Zero), wy71)) → new_takeWhile113(wy71)
new_takeWhile113(:(Neg(Succ(wy7000)), wy71)) → new_takeWhile110(Zero, wy7000, wy71)
new_takeWhile111(wy339, wy340, :(Neg(Succ(wy341000)), wy3411), Zero, Succ(wy3430)) → new_takeWhile110(Succ(wy339), wy341000, wy3411)
new_takeWhile(:(Pos(Zero), wy71)) → new_takeWhile(wy71)
new_takeWhile111(wy339, wy340, wy341, Zero, Zero) → new_takeWhile112(wy339, wy340, wy341)
new_takeWhile111(wy339, wy340, wy341, Succ(wy3420), Succ(wy3430)) → new_takeWhile111(wy339, wy340, wy341, wy3420, wy3430)
new_takeWhile113(:(Pos(Zero), wy71)) → new_takeWhile(wy71)
new_takeWhile(:(Neg(Zero), wy71)) → new_takeWhile113(wy71)
new_takeWhile110(Succ(wy1900), wy21, wy138) → new_takeWhile111(wy1900, wy21, wy138, wy1900, wy21)
new_takeWhile(:(Neg(Succ(wy7000)), wy71)) → new_takeWhile110(Zero, wy7000, wy71)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 2 SCCs.
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ Narrow
Q DP problem:
The TRS P consists of the following rules:
new_takeWhile110(Zero, wy21, wy138) → new_takeWhile(wy138)
new_takeWhile113(:(Neg(Zero), wy71)) → new_takeWhile113(wy71)
new_takeWhile113(:(Neg(Succ(wy7000)), wy71)) → new_takeWhile110(Zero, wy7000, wy71)
new_takeWhile(:(Pos(Zero), wy71)) → new_takeWhile(wy71)
new_takeWhile113(:(Pos(Zero), wy71)) → new_takeWhile(wy71)
new_takeWhile(:(Neg(Zero), wy71)) → new_takeWhile113(wy71)
new_takeWhile(:(Neg(Succ(wy7000)), wy71)) → new_takeWhile110(Zero, wy7000, wy71)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_takeWhile(:(Pos(Zero), wy71)) → new_takeWhile(wy71)
The graph contains the following edges 1 > 1
- new_takeWhile113(:(Pos(Zero), wy71)) → new_takeWhile(wy71)
The graph contains the following edges 1 > 1
- new_takeWhile110(Zero, wy21, wy138) → new_takeWhile(wy138)
The graph contains the following edges 3 >= 1
- new_takeWhile(:(Neg(Zero), wy71)) → new_takeWhile113(wy71)
The graph contains the following edges 1 > 1
- new_takeWhile(:(Neg(Succ(wy7000)), wy71)) → new_takeWhile110(Zero, wy7000, wy71)
The graph contains the following edges 1 > 2, 1 > 3
- new_takeWhile113(:(Neg(Zero), wy71)) → new_takeWhile113(wy71)
The graph contains the following edges 1 > 1
- new_takeWhile113(:(Neg(Succ(wy7000)), wy71)) → new_takeWhile110(Zero, wy7000, wy71)
The graph contains the following edges 1 > 2, 1 > 3
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ Narrow
Q DP problem:
The TRS P consists of the following rules:
new_takeWhile112(wy339, wy340, :(Neg(Succ(wy341000)), wy3411)) → new_takeWhile110(Succ(wy339), wy341000, wy3411)
new_takeWhile111(wy339, wy340, :(Neg(Succ(wy341000)), wy3411), Zero, Succ(wy3430)) → new_takeWhile110(Succ(wy339), wy341000, wy3411)
new_takeWhile111(wy339, wy340, wy341, Zero, Zero) → new_takeWhile112(wy339, wy340, wy341)
new_takeWhile111(wy339, wy340, wy341, Succ(wy3420), Succ(wy3430)) → new_takeWhile111(wy339, wy340, wy341, wy3420, wy3430)
new_takeWhile110(Succ(wy1900), wy21, wy138) → new_takeWhile111(wy1900, wy21, wy138, wy1900, wy21)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_takeWhile111(wy339, wy340, :(Neg(Succ(wy341000)), wy3411), Zero, Succ(wy3430)) → new_takeWhile110(Succ(wy339), wy341000, wy3411)
The graph contains the following edges 3 > 2, 3 > 3
- new_takeWhile112(wy339, wy340, :(Neg(Succ(wy341000)), wy3411)) → new_takeWhile110(Succ(wy339), wy341000, wy3411)
The graph contains the following edges 3 > 2, 3 > 3
- new_takeWhile110(Succ(wy1900), wy21, wy138) → new_takeWhile111(wy1900, wy21, wy138, wy1900, wy21)
The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 3, 1 > 4, 2 >= 5
- new_takeWhile111(wy339, wy340, wy341, Succ(wy3420), Succ(wy3430)) → new_takeWhile111(wy339, wy340, wy341, wy3420, wy3430)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 > 4, 5 > 5
- new_takeWhile111(wy339, wy340, wy341, Zero, Zero) → new_takeWhile112(wy339, wy340, wy341)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDP
↳ Narrow
Q DP problem:
The TRS P consists of the following rules:
new_takeWhile118(wy60, wy59) → new_takeWhile116(Zero, wy60, wy59)
new_takeWhile116(wy50, wy60, :(wy590, wy591)) → new_takeWhile117(wy50, wy590, wy591, wy590)
new_takeWhile117(Succ(wy500), wy60, wy59, Pos(Zero)) → new_takeWhile114(wy500, wy60, wy59, Zero, Succ(wy500))
new_takeWhile114(wy355, wy356, wy357, Zero, Zero) → new_takeWhile116(Succ(wy355), wy356, wy357)
new_takeWhile117(Zero, wy60, wy59, Pos(Zero)) → new_takeWhile116(Zero, wy60, wy59)
new_takeWhile117(Zero, wy60, wy59, Neg(Zero)) → new_takeWhile118(wy60, wy59)
new_takeWhile117(Succ(wy500), wy60, wy59, Neg(Zero)) → new_takeWhile115(Succ(wy500), wy60, wy59)
new_takeWhile114(wy355, wy356, wy357, Succ(wy3580), Succ(wy3590)) → new_takeWhile114(wy355, wy356, wy357, wy3580, wy3590)
new_takeWhile117(Succ(wy500), wy60, wy59, Pos(Succ(wy6200))) → new_takeWhile114(wy500, wy60, wy59, wy6200, wy500)
new_takeWhile117(wy50, wy60, :(wy590, wy591), Neg(Succ(wy6200))) → new_takeWhile117(wy50, wy590, wy591, wy590)
new_takeWhile115(wy50, wy60, :(wy590, wy591)) → new_takeWhile117(wy50, wy590, wy591, wy590)
new_takeWhile114(wy355, wy356, wy357, Zero, Succ(wy3590)) → new_takeWhile115(Succ(wy355), wy356, wy357)
new_takeWhile119(Succ(wy500), wy60, wy59, wy6200) → new_takeWhile114(wy500, wy60, wy59, wy6200, wy500)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ Narrow
Q DP problem:
The TRS P consists of the following rules:
new_takeWhile117(Succ(wy500), wy60, wy59, Pos(Succ(wy6200))) → new_takeWhile114(wy500, wy60, wy59, wy6200, wy500)
new_takeWhile118(wy60, wy59) → new_takeWhile116(Zero, wy60, wy59)
new_takeWhile116(wy50, wy60, :(wy590, wy591)) → new_takeWhile117(wy50, wy590, wy591, wy590)
new_takeWhile117(wy50, wy60, :(wy590, wy591), Neg(Succ(wy6200))) → new_takeWhile117(wy50, wy590, wy591, wy590)
new_takeWhile117(Succ(wy500), wy60, wy59, Pos(Zero)) → new_takeWhile114(wy500, wy60, wy59, Zero, Succ(wy500))
new_takeWhile114(wy355, wy356, wy357, Zero, Zero) → new_takeWhile116(Succ(wy355), wy356, wy357)
new_takeWhile117(Zero, wy60, wy59, Neg(Zero)) → new_takeWhile118(wy60, wy59)
new_takeWhile117(Zero, wy60, wy59, Pos(Zero)) → new_takeWhile116(Zero, wy60, wy59)
new_takeWhile115(wy50, wy60, :(wy590, wy591)) → new_takeWhile117(wy50, wy590, wy591, wy590)
new_takeWhile117(Succ(wy500), wy60, wy59, Neg(Zero)) → new_takeWhile115(Succ(wy500), wy60, wy59)
new_takeWhile114(wy355, wy356, wy357, Zero, Succ(wy3590)) → new_takeWhile115(Succ(wy355), wy356, wy357)
new_takeWhile114(wy355, wy356, wy357, Succ(wy3580), Succ(wy3590)) → new_takeWhile114(wy355, wy356, wy357, wy3580, wy3590)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_takeWhile117(Zero, wy60, wy59, Pos(Zero)) → new_takeWhile116(Zero, wy60, wy59)
The graph contains the following edges 1 >= 1, 4 > 1, 2 >= 2, 3 >= 3
- new_takeWhile117(wy50, wy60, :(wy590, wy591), Neg(Succ(wy6200))) → new_takeWhile117(wy50, wy590, wy591, wy590)
The graph contains the following edges 1 >= 1, 3 > 2, 3 > 3, 3 > 4
- new_takeWhile114(wy355, wy356, wy357, Zero, Succ(wy3590)) → new_takeWhile115(Succ(wy355), wy356, wy357)
The graph contains the following edges 2 >= 2, 3 >= 3
- new_takeWhile114(wy355, wy356, wy357, Succ(wy3580), Succ(wy3590)) → new_takeWhile114(wy355, wy356, wy357, wy3580, wy3590)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 > 4, 5 > 5
- new_takeWhile115(wy50, wy60, :(wy590, wy591)) → new_takeWhile117(wy50, wy590, wy591, wy590)
The graph contains the following edges 1 >= 1, 3 > 2, 3 > 3, 3 > 4
- new_takeWhile116(wy50, wy60, :(wy590, wy591)) → new_takeWhile117(wy50, wy590, wy591, wy590)
The graph contains the following edges 1 >= 1, 3 > 2, 3 > 3, 3 > 4
- new_takeWhile117(Succ(wy500), wy60, wy59, Neg(Zero)) → new_takeWhile115(Succ(wy500), wy60, wy59)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3
- new_takeWhile117(Zero, wy60, wy59, Neg(Zero)) → new_takeWhile118(wy60, wy59)
The graph contains the following edges 2 >= 1, 3 >= 2
- new_takeWhile118(wy60, wy59) → new_takeWhile116(Zero, wy60, wy59)
The graph contains the following edges 1 >= 2, 2 >= 3
- new_takeWhile114(wy355, wy356, wy357, Zero, Zero) → new_takeWhile116(Succ(wy355), wy356, wy357)
The graph contains the following edges 2 >= 2, 3 >= 3
- new_takeWhile117(Succ(wy500), wy60, wy59, Pos(Succ(wy6200))) → new_takeWhile114(wy500, wy60, wy59, wy6200, wy500)
The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 3, 4 > 4, 1 > 5
- new_takeWhile117(Succ(wy500), wy60, wy59, Pos(Zero)) → new_takeWhile114(wy500, wy60, wy59, Zero, Succ(wy500))
The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 3, 4 > 4, 1 >= 5
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ Narrow
Q DP problem:
The TRS P consists of the following rules:
new_takeWhile120(wy235, wy236, wy237, Succ(wy2380), Succ(wy2390), wy240) → new_takeWhile120(wy235, wy236, wy237, wy2380, wy2390, wy240)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_takeWhile120(wy235, wy236, wy237, Succ(wy2380), Succ(wy2390), wy240) → new_takeWhile120(wy235, wy236, wy237, wy2380, wy2390, wy240)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 > 4, 5 > 5, 6 >= 6
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ Narrow
Q DP problem:
The TRS P consists of the following rules:
new_takeWhile121(wy218, wy219, wy220, Succ(wy2210), Succ(wy2220), wy223) → new_takeWhile121(wy218, wy219, wy220, wy2210, wy2220, wy223)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_takeWhile121(wy218, wy219, wy220, Succ(wy2210), Succ(wy2220), wy223) → new_takeWhile121(wy218, wy219, wy220, wy2210, wy2220, wy223)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 > 4, 5 > 5, 6 >= 6
Haskell To QDPs